es:ES, L:(Id List).
fischer(L)
 (e1:E, j:Id.
 Newround(e1)
  (j  L)
  ((j = loc(e1)))
  (sender(the rcv(free message from e1 to j)) = e1)) 

latex

Definitions	, P & Q, IdLnk, t  T, P  Q, P  Q, "$x", the rcv(free message from e1 to j), P  Q, Id, x:A. B(x), False, if b then t else f fi , ff, eq_atom$n(x;y), Atom2Deq, IdDeq, t.1, eqof(d), a = b, x:A. B(x), b, xL. P(x), P  Q, A c B, Newround(e), fischer(L)
Lemmas	event system wf, fischer wf, f-newround wf, l member wf, es-loc wf, Id wf, not wf, assert-eq-id, es-sender-first-from, es-E wf